The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

p(s(x)) → x [1]
p(0) → 0 [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y) [1]
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y) [1]
if(false, b1, b2, b3, x, y) → average(p(x), s(y)) [1]
if2(true, b2, b3, x, y) → 0 [1]
if2(false, b2, b3, x, y) → if3(b2, b3, x, y) [1]
if3(true, b3, x, y) → 0 [1]
if3(false, b3, x, y) → if4(b3, x, y) [1]
if4(true, x, y) → s(0) [1]
if4(false, x, y) → average(s(x), p(p(y))) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

p(s(x)) → x [1]
p(0) → 0 [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y) [1]
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y) [1]
if(false, b1, b2, b3, x, y) → average(p(x), s(y)) [1]
if2(true, b2, b3, x, y) → 0 [1]
if2(false, b2, b3, x, y) → if3(b2, b3, x, y) [1]
if3(true, b3, x, y) → 0 [1]
if3(false, b3, x, y) → if4(b3, x, y) [1]
if4(true, x, y) → s(0) [1]
if4(false, x, y) → average(s(x), p(p(y))) [1]

The TRS has the following type information:

p :: s:0 → s:0 s :: s:0 → s:0 0 :: s:0 le :: s:0 → s:0 → true:false true :: true:false false :: true:false average :: s:0 → s:0 → s:0 if :: true:false → true:false → true:false → true:false → s:0 → s:0 → s:0 if2 :: true:false → true:false → true:false → s:0 → s:0 → s:0 if3 :: true:false → true:false → s:0 → s:0 → s:0 if4 :: true:false → s:0 → s:0 → s:0

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: p(s(x)) → x [1] p(0) → 0 [1] le(0, y) → true [1] le(s(x), 0) → false [1] le(s(x), s(y)) → le(x, y) [1] average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y) [1] if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y) [1] if(false, b1, b2, b3, x, y) → average(p(x), s(y)) [1] if2(true, b2, b3, x, y) → 0 [1] if2(false, b2, b3, x, y) → if3(b2, b3, x, y) [1] if3(true, b3, x, y) → 0 [1] if3(false, b3, x, y) → if4(b3, x, y) [1] if4(true, x, y) → s(0) [1] if4(false, x, y) → average(s(x), p(p(y))) [1] The TRS has the following type information: p :: s:0 → s:0 s :: s:0 → s:0 0 :: s:0 le :: s:0 → s:0 → true:false true :: true:false false :: true:false average :: s:0 → s:0 → s:0 if :: true:false → true:false → true:false → true:false → s:0 → s:0 → s:0 if2 :: true:false → true:false → true:false → s:0 → s:0 → s:0 if3 :: true:false → true:false → s:0 → s:0 → s:0 if4 :: true:false → s:0 → s:0 → s:0 Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 1
false => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

average(z, z') -{ 1 }→ if(le(x, 0), le(y, 0), le(y, 1 + 0), le(y, 1 + (1 + 0)), x, y) :|: x >= 0, y >= 0, z = x, z' = y
if(z, z', z'', z1, z2, z3) -{ 1 }→ if2(b1, b2, b3, x, y) :|: b2 >= 0, z2 = x, b1 >= 0, z = 1, z1 = b3, z3 = y, x >= 0, y >= 0, z' = b1, z'' = b2, b3 >= 0
if(z, z', z'', z1, z2, z3) -{ 1 }→ average(p(x), 1 + y) :|: b2 >= 0, z2 = x, b1 >= 0, z1 = b3, z3 = y, x >= 0, y >= 0, z' = b1, z = 0, z'' = b2, b3 >= 0
if2(z, z', z'', z1, z2) -{ 1 }→ if3(b2, b3, x, y) :|: b2 >= 0, z2 = y, x >= 0, y >= 0, z' = b2, z = 0, z'' = b3, z1 = x, b3 >= 0
if2(z, z', z'', z1, z2) -{ 1 }→ 0 :|: b2 >= 0, z2 = y, z = 1, x >= 0, y >= 0, z' = b2, z'' = b3, z1 = x, b3 >= 0
if3(z, z', z'', z1) -{ 1 }→ if4(b3, x, y) :|: z1 = y, z' = b3, x >= 0, y >= 0, z'' = x, z = 0, b3 >= 0
if3(z, z', z'', z1) -{ 1 }→ 0 :|: z1 = y, z' = b3, z = 1, x >= 0, y >= 0, z'' = x, b3 >= 0
if4(z, z', z'') -{ 1 }→ average(1 + x, p(p(y))) :|: z' = x, z'' = y, x >= 0, y >= 0, z = 0
if4(z, z', z'') -{ 1 }→ 1 + 0 :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
p(z) -{ 1 }→ x :|: x >= 0, z = 1 + x
p(z) -{ 1 }→ 0 :|: z = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V2, V9, V10, V11, V12),0,[p(V, Out)],[V >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[average(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[if(V, V2, V9, V10, V11, V12, Out)],[V >= 0,V2 >= 0,V9 >= 0,V10 >= 0,V11 >= 0,V12 >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[if2(V, V2, V9, V10, V11, Out)],[V >= 0,V2 >= 0,V9 >= 0,V10 >= 0,V11 >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[if3(V, V2, V9, V10, Out)],[V >= 0,V2 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V2, V9, V10, V11, V12),0,[if4(V, V2, V9, Out)],[V >= 0,V2 >= 0,V9 >= 0]). eq(p(V, Out),1,[],[Out = V1,V1 >= 0,V = 1 + V1]). eq(p(V, Out),1,[],[Out = 0,V = 0]). eq(le(V, V2, Out),1,[],[Out = 1,V3 >= 0,V = 0,V2 = V3]). eq(le(V, V2, Out),1,[],[Out = 0,V4 >= 0,V = 1 + V4,V2 = 0]). eq(le(V, V2, Out),1,[le(V5, V6, Ret)],[Out = Ret,V2 = 1 + V6,V5 >= 0,V6 >= 0,V = 1 + V5]). eq(average(V, V2, Out),1,[le(V7, 0, Ret0),le(V8, 0, Ret1),le(V8, 1 + 0, Ret2),le(V8, 1 + (1 + 0), Ret3),if(Ret0, Ret1, Ret2, Ret3, V7, V8, Ret4)],[Out = Ret4,V7 >= 0,V8 >= 0,V = V7,V2 = V8]). eq(if(V, V2, V9, V10, V11, V12, Out),1,[if2(V13, V14, V15, V16, V17, Ret5)],[Out = Ret5,V14 >= 0,V11 = V16,V13 >= 0,V = 1,V10 = V15,V12 = V17,V16 >= 0,V17 >= 0,V2 = V13,V9 = V14,V15 >= 0]). eq(if(V, V2, V9, V10, V11, V12, Out),1,[p(V18, Ret01),average(Ret01, 1 + V19, Ret6)],[Out = Ret6,V20 >= 0,V11 = V18,V21 >= 0,V10 = V22,V12 = V19,V18 >= 0,V19 >= 0,V2 = V21,V = 0,V9 = V20,V22 >= 0]). eq(if2(V, V2, V9, V10, V11, Out),1,[],[Out = 0,V23 >= 0,V11 = V24,V = 1,V25 >= 0,V24 >= 0,V2 = V23,V9 = V26,V10 = V25,V26 >= 0]). eq(if2(V, V2, V9, V10, V11, Out),1,[if3(V27, V28, V29, V30, Ret7)],[Out = Ret7,V27 >= 0,V11 = V30,V29 >= 0,V30 >= 0,V2 = V27,V = 0,V9 = V28,V10 = V29,V28 >= 0]). eq(if3(V, V2, V9, V10, Out),1,[],[Out = 0,V10 = V31,V2 = V32,V = 1,V33 >= 0,V31 >= 0,V9 = V33,V32 >= 0]). eq(if3(V, V2, V9, V10, Out),1,[if4(V34, V35, V36, Ret8)],[Out = Ret8,V10 = V36,V2 = V34,V35 >= 0,V36 >= 0,V9 = V35,V = 0,V34 >= 0]). eq(if4(V, V2, V9, Out),1,[],[Out = 1,V2 = V37,V9 = V38,V = 1,V37 >= 0,V38 >= 0]). eq(if4(V, V2, V9, Out),1,[p(V40, Ret10),p(Ret10, Ret11),average(1 + V39, Ret11, Ret9)],[Out = Ret9,V2 = V39,V9 = V40,V39 >= 0,V40 >= 0,V = 0]). input_output_vars(p(V,Out),[V],[Out]). input_output_vars(le(V,V2,Out),[V,V2],[Out]). input_output_vars(average(V,V2,Out),[V,V2],[Out]). input_output_vars(if(V,V2,V9,V10,V11,V12,Out),[V,V2,V9,V10,V11,V12],[Out]). input_output_vars(if2(V,V2,V9,V10,V11,Out),[V,V2,V9,V10,V11],[Out]). input_output_vars(if3(V,V2,V9,V10,Out),[V,V2,V9,V10],[Out]). input_output_vars(if4(V,V2,V9,Out),[V,V2,V9],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [p/2]
1. recursive : [le/3]
2. recursive : [average/3,if/7,if2/6,if3/5,if4/4]
3. non_recursive : [start/6]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into p/2
1. SCC is partially evaluated into le/3
2. SCC is partially evaluated into average/3
3. SCC is partially evaluated into start/6

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations p/2
* CE 16 is refined into CE [26]
* CE 17 is refined into CE [27]


### Cost equations --> "Loop" of p/2
* CEs [26] --> Loop 17
* CEs [27] --> Loop 18

### Ranking functions of CR p(V,Out)

#### Partial ranking functions of CR p(V,Out)


### Specialization of cost equations le/3
* CE 25 is refined into CE [28]
* CE 24 is refined into CE [29]
* CE 23 is refined into CE [30]


### Cost equations --> "Loop" of le/3
* CEs [29] --> Loop 19
* CEs [30] --> Loop 20
* CEs [28] --> Loop 21

### Ranking functions of CR le(V,V2,Out)
* RF of phase [21]: [V,V2]

#### Partial ranking functions of CR le(V,V2,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V2


### Specialization of cost equations average/3
* CE 19 is refined into CE [31]
* CE 18 is refined into CE [32]
* CE 22 is refined into CE [33]
* CE 21 is refined into CE [34,35,36,37]
* CE 20 is refined into CE [38]


### Cost equations --> "Loop" of average/3
* CEs [35] --> Loop 22
* CEs [36] --> Loop 23
* CEs [37] --> Loop 24
* CEs [34] --> Loop 25
* CEs [38] --> Loop 26
* CEs [31] --> Loop 27
* CEs [32] --> Loop 28
* CEs [33] --> Loop 29

### Ranking functions of CR average(V,V2,Out)
* RF of phase [22,23,24,26]: [3*V+2*V2-4]

#### Partial ranking functions of CR average(V,V2,Out)
* Partial RF of phase [22,23,24,26]:
- RF of loop [22:1,23:1,24:1]:
V depends on loops [26:1]
- RF of loop [23:1]:
-V2+3 depends on loops [26:1]
- RF of loop [24:1]:
-V2+2 depends on loops [26:1]
- RF of loop [26:1]:
-V+1 depends on loops [22:1,23:1,24:1]
V2/2-1 depends on loops [22:1,23:1,24:1]


### Specialization of cost equations start/6
* CE 11 is refined into CE [39]
* CE 2 is refined into CE [40]
* CE 5 is refined into CE [41]
* CE 4 is refined into CE [42]
* CE 7 is refined into CE [43,44,45,46,47,48,49]
* CE 3 is refined into CE [50]
* CE 6 is refined into CE [51]
* CE 8 is refined into CE [52,53,54,55,56,57,58]
* CE 9 is refined into CE [59,60,61,62,63,64,65]
* CE 10 is refined into CE [66,67,68,69,70,71]
* CE 12 is refined into CE [72,73,74,75,76,77,78]
* CE 13 is refined into CE [79,80]
* CE 14 is refined into CE [81,82,83,84]
* CE 15 is refined into CE [85,86,87,88,89,90]


### Cost equations --> "Loop" of start/6
* CEs [90] --> Loop 30
* CEs [39,42] --> Loop 31
* CEs [40,41,43,44,45,46,47,48,49,80,82,83,84,88,89] --> Loop 32
* CEs [50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,81,85,86,87] --> Loop 33

### Ranking functions of CR start(V,V2,V9,V10,V11,V12)

#### Partial ranking functions of CR start(V,V2,V9,V10,V11,V12)


Computing Bounds
=====================================

#### Cost of chains of p(V,Out):
* Chain [18]: 1
with precondition: [V=0,Out=0]

* Chain [17]: 1
with precondition: [V=Out+1,V>=1]


#### Cost of chains of le(V,V2,Out):
* Chain [[21],20]: 1*it(21)+1
Such that:it(21) =< V

with precondition: [Out=1,V>=1,V2>=V]

* Chain [[21],19]: 1*it(21)+1
Such that:it(21) =< V2

with precondition: [Out=0,V2>=1,V>=V2+1]

* Chain [20]: 1
with precondition: [V=0,Out=1,V2>=0]

* Chain [19]: 1
with precondition: [V2=0,Out=0,V>=1]


#### Cost of chains of average(V,V2,Out):
* Chain [[22,23,24,26],27]: 37*it(22)+1*s(1)+1*s(2)+3*s(20)+9
Such that:s(1) =< 1
s(2) =< 2
aux(28) =< 3*V+2*V2
it(22) =< aux(28)
s(20) =< aux(28)*2

with precondition: [Out=1,V>=0,V2>=1,V2+2*V>=3]

* Chain [29]: 7
with precondition: [V=0,V2=0,Out=0]

* Chain [28]: 2*s(27)+8
Such that:aux(29) =< 1
s(27) =< aux(29)

with precondition: [V=0,V2=1,Out=0]

* Chain [27]: 1*s(1)+1*s(2)+9
Such that:s(1) =< 1
s(2) =< 2

with precondition: [V=0,V2=2,Out=1]

* Chain [25,[22,23,24,26],27]: 37*it(22)+1*s(1)+1*s(2)+3*s(20)+16
Such that:s(1) =< 1
s(2) =< 2
aux(28) =< 3*V
it(22) =< aux(28)
s(20) =< aux(28)*2

with precondition: [V2=0,Out=1,V>=2]

* Chain [25,28]: 2*s(27)+15
Such that:aux(29) =< 1
s(27) =< aux(29)

with precondition: [V=1,V2=0,Out=0]


#### Cost of chains of start(V,V2,V9,V10,V11,V12):
* Chain [33]: 41*s(30)+17*s(32)+111*s(34)+9*s(35)+37*s(53)+3*s(54)+111*s(60)+9*s(61)+37*s(79)+3*s(80)+37*s(88)+3*s(89)+37*s(97)+3*s(98)+111*s(104)+9*s(105)+37*s(123)+3*s(124)+21
Such that:s(122) =< 3*V2+2*V9
s(78) =< 3*V9+2*V10
s(52) =< 3*V10+2*V11
s(96) =< 3*V11+2*V12
s(87) =< 2*V12+2
aux(30) =< 1
aux(31) =< 2
aux(32) =< 3*V2+3
aux(33) =< 3*V9+3
aux(34) =< 3*V10+3
s(30) =< aux(30)
s(32) =< aux(31)
s(34) =< aux(34)
s(35) =< aux(34)*2
s(53) =< s(52)
s(54) =< s(52)*2
s(60) =< aux(33)
s(61) =< aux(33)*2
s(79) =< s(78)
s(80) =< s(78)*2
s(88) =< s(87)
s(89) =< s(87)*2
s(97) =< s(96)
s(98) =< s(96)*2
s(104) =< aux(32)
s(105) =< aux(32)*2
s(123) =< s(122)
s(124) =< s(122)*2

with precondition: [V=0]

* Chain [32]: 13*s(130)+5*s(132)+111*s(134)+9*s(135)+37*s(153)+3*s(154)+1*s(155)+1*s(156)+37*s(162)+3*s(163)+22
Such that:s(156) =< V
s(161) =< 3*V
s(155) =< V2
s(152) =< 3*V11+2*V12
aux(35) =< 1
aux(36) =< 2
aux(37) =< 3*V11+3
s(130) =< aux(35)
s(132) =< aux(36)
s(134) =< aux(37)
s(135) =< aux(37)*2
s(153) =< s(152)
s(154) =< s(152)*2
s(162) =< s(161)
s(163) =< s(161)*2

with precondition: [V>=1]

* Chain [31]: 2
with precondition: [V=1,V2>=0,V9>=0]

* Chain [30]: 1*s(164)+1*s(165)+37*s(167)+3*s(168)+9
Such that:s(164) =< 1
s(165) =< 2
s(166) =< 3*V+2*V2
s(167) =< s(166)
s(168) =< s(166)*2

with precondition: [V>=0,V2>=1,V2+2*V>=3]


Closed-form bounds of start(V,V2,V9,V10,V11,V12):
-------------------------------------
* Chain [33] with precondition: [V=0]
- Upper bound: nat(2*V12+2)*43+96+nat(3*V2+3)*129+nat(3*V2+2*V9)*43+nat(3*V9+3)*129+nat(3*V9+2*V10)*43+nat(3*V10+3)*129+nat(3*V10+2*V11)*43+nat(3*V11+2*V12)*43
- Complexity: n
* Chain [32] with precondition: [V>=1]
- Upper bound: V+45+nat(V2)+129*V+nat(3*V11+3)*129+nat(3*V11+2*V12)*43
- Complexity: n
* Chain [31] with precondition: [V=1,V2>=0,V9>=0]
- Upper bound: 2
- Complexity: constant
* Chain [30] with precondition: [V>=0,V2>=1,V2+2*V>=3]
- Upper bound: 129*V+86*V2+12
- Complexity: n

### Maximum cost of start(V,V2,V9,V10,V11,V12): max([nat(3*V+2*V2)*43+10,nat(3*V11+2*V12)*43+43+max([nat(V2)+V+129*V+nat(3*V11+3)*129,nat(2*V12+2)*43+51+nat(3*V2+3)*129+nat(3*V2+2*V9)*43+nat(3*V9+3)*129+nat(3*V9+2*V10)*43+nat(3*V10+3)*129+nat(3*V10+2*V11)*43])])+2
Asymptotic class: n
* Total analysis performed in 639 ms.

(10) BOUNDS(1, n^1)